\begin{tabbing}
$\forall$$M$:MsgA.
\\[0ex]\{\=1of($M$) $\in$ $a$:Id fp$\rightarrow$ Type \& 1of(2of($M$)) $\in$ $k$:Knd fp$\rightarrow$ Type\+
\\[0ex]\& 1of(2of(2of($M$))) $\in$ $x$:Id fp$\rightarrow$ 1of($M$)($x$)?Void
\\[0ex]\& 1of(2of(2of(2of($M$)))) $\in$ $a$:Id fp$\rightarrow$ State(1of($M$))$\rightarrow$1of(2of($M$))(locl($a$))?Top$\rightarrow$Prop
\\[0ex]\& \=1of(2of(2of(2of(2of($M$)))))\+
\\[0ex]$\in$ ${\it kx}$:Knd$\times$Id fp$\rightarrow$ State(1of($M$))$\rightarrow$Valtype(1of(2of($M$));1of(${\it kx}$))$\rightarrow$1of($M$)(2of(${\it kx}$))?Void
\-\\[0ex]\& \=1of(2of(2of(2of(2of(2of($M$))))))\+
\\[0ex]$\in$ \=${\it kl}$:Knd$\times$IdLnk fp$\rightarrow$\+
\\[0ex](\=${\it tg}$:Id\+
\\[0ex]$\times$(\=State(1of($M$))$\rightarrow$Valtype(1of(2of($M$));1of(${\it kl}$))$\rightarrow$\+
\\[0ex](1of(2of($M$))(rcv(2of(${\it kl}$),${\it tg}$))?Void List))) List
\-\-\-\-\\[0ex]\& 1of(2of(2of(2of(2of(2of(2of($M$))))))) $\in$ $x$:Id fp$\rightarrow$ Knd List
\\[0ex]\& 1of(2of(2of(2of(2of(2of(2of(2of($M$)))))))) $\in$ ${\it ltg}$:IdLnk$\times$Id fp$\rightarrow$ Knd List\}
\-
\end{tabbing}